$LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
require 'ext_pr1_v4'


#Konstanten
MIN_IN_SEC   = 60
HOUR_IN_MIN  = 60
HOURS_OF_DAY = 24
HOURS_OF_HALF_DAY = HOURS_OF_DAY/2
HOUR_IN_SEC  = MIN_IN_SEC * HOUR_IN_MIN
DAY_IN_SEC   = HOUR_IN_SEC * HOURS_OF_DAY

#Typ-Prädikate
def hour24?(value) (value.int? and value.in?(0...HOURS_OF_DAY)) end
def hour12?(value) (value.int? and value.in?(1..HOURS_OF_HALF_DAY)) end
def min?(value)    (value.int? and value.in?(0...HOUR_IN_MIN)) end
def sec?(value)    (value.int? and value.in?(0...MIN_IN_SEC)) end
#def halve?(value)  (value.symbol? and (value == :PM or value == :AM)) end
def halve?(value)  (value.symbol? and value.in?([:PM, :AM])) end
def day_in_sec?(value) (value.int? and value.in?(0..DAY_IN_SEC)) end


################################### Schritt 1
# :ClockSec ::= (seconds) ::
# int => ClockSec :: 0...DAY_IN_SEC

#ClockSec[-1] => ERROR
#ClockSec[86401] => ERROR
def_class(:ClockSec,[:seconds]) {
  def invariant?
    day_in_sec?(seconds)
  end
}

# clock_sec_add ::= (ClockSec[Current],ClockSec[delta]) ::
# ClockSec x ClockSec => ClockSec

#
# clock_sec_add(ClockSec[0],ClockSec[0]) => ClockSec[0]
# clock_sec_add(ClockSec[1],ClockSec[0]) => ClockSec[1]
# clock_sec_add(ClockSec[0],ClockSec[1]) => ClockSec[1]
# clock_sec_add(ClockSec[1],ClockSec[1]) => ClockSec[2]
# clock_sec_add(ClockSec[86399],ClockSec[1]) => ClockSec[86400]
# clock_sec_add(ClockSec[86400],ClockSec[1]) => ERROR 
# clock_sec_add(ClockSec[1],ClockSec[86400]) => ERROR

def clock_sec_add(current,delta)
   check_pre((current.clock_sec? and delta.clock_sec?))
   ClockSec[current.seconds + delta.seconds]
end

# clock_sec_sub ::= (ClockSec[Current],ClockSec[delta]) ::
# ClockSec x ClockSec => ClockSec

# clock_sec_sub(ClockSec[11],ClockSec[1]) => ClockSec[10]
# clock_sec_sub(ClockSec[1],ClockSec[1]) => ClockSec[0]
# clock_sec_sub(ClockSec[0],ClockSec[1]) => ERROR
def clock_sec_sub(current,delta)
   check_pre((current.clock_sec? and delta.clock_sec?))
   ClockSec[current.seconds - delta.seconds]
end

# clock_sec_succ ::= (ClockSec[seconds]) ::
# ClockSec => ClockSec

# clock_sec_succ(ClockSec[0]) => ClockSec[1]
# clock_sec_succ(ClockSec[1]) => ClockSec[2]
# clock_sec_succ(ClockSec[86399]) => ClockSec[86400]
# clock_sec_succ(ClockSec[86400]) => ERROR
def clock_sec_succ(seconds)
   check_pre((seconds.clock_sec?))
   ClockSec[seconds.seconds+1]
end

# clock_sec_pred ::= (ClockSec[seconds]) ::
# ClockSec => ClockSec

# clock_sec_pred(ClockSec[86400]) => ClockSec[86399]
# clock_sec_pred(ClockSec[1]) => ClockSec[0]
# clock_sec_pred(ClockSec[0]) => ERROR
def clock_sec_pred(seconds)
   check_pre((seconds.clock_sec?))
   ClockSec[seconds.seconds-1]
end

################################### Schritt 2
# Clock24 ::= Clock24[hour,min,sec] :: 
# Hour x Min x Sec

# Clock24[00,00,00] => Clock24[00,00,00]
# Clock24[00,00,59] => Clock24[00,00,59]
# Clock24[00,59,00] => Clock24[00,59,00]
# Clock24[23,00,00] => Clock24[23,00,00]
# Clock24[23,59,59] => Clock24[23,59,59]
# Clock24[24,00,00] => ERROR
# Clock24[00,60,00] => ERROR
# Clock24[00,00,60] => ERROR
# Clock24[-1,00,00] => ERROR
# Clock24[00,-1,00] => ERROR
# Clock24[00,00,-1] => ERROR
def_class(:Clock24,[:hour,:min,:sec]) {
  def invariant?
    hour24?(hour) and min?(min) and sec?(sec)
  end
}

# Clock12 ::= Clock12[halve,hour,min,sec] :: 
# Halve x Hour x Min x Sec

# Clock12[:PM,1,00,00] => Clock12[:PM,1,00,00]
# Clock12[:PM,12,00,00] => Clock12[:PM,12,00,00]
# Clock12[:PM,12,59,00] => Clock12[:PM,12,59,00]
# Clock12[:PM,12,59,59] => Clock12[:PM,12,59,59]
# 
# Clock12[:AM,12,00,00] => Clock12[:AM,12,00,00]
# Clock12[:AM,12,59,00] => Clock12[:AM,12,59,00]
# Clock12[:AM,12,59,59] => Clock12[:AM,12,59,59]
# 
# Clock12[:AM,00,00,00] => ERROR
# Clock12[:AM,13,00,00] => ERROR
# Clock12[:AM,12,60,00] => ERROR
# Clock12[:AM,12,00,60] => ERROR
# Clock12[:PM,00,00,00] => ERROR
# Clock12[:PM,13,00,00] => ERROR
# Clock12[:PM,12,60,00] => ERROR
# Clock12[:PM,12,00,60] => ERROR
def_class(:Clock12,[:halve,:hour,:min,:sec]) {
  def invariant?
    hour12?(hour) and min?(min) and sec?(sec) and halve?(halve)
  end
}


################################### Schritt 3
# clock24_to_clock_sec ::= (clock) ::
# Clock24 => ClockSec

# clock24_to_clock_sec(Clock24[0,0,0]) => ClockSec[0]
# clock24_to_clock_sec(Clock24[0,0,1]) => ClockSec[1]
# clock24_to_clock_sec(Clock24[0,1,0]) => ClockSec[60]
# clock24_to_clock_sec(Clock24[1,0,0]) => ClockSec[3600]
def clock24_to_clock_sec(clock)
   check_pre((clock.clock24?))
   ClockSec[(clock.hour*HOUR_IN_SEC) + (clock.min*MIN_IN_SEC) + clock.sec]
end

# clock12_to_clock_sec ::= (clock) ::
# Clock12 => ClockSec

# clock12_to_clock_sec(Clock12[:AM,12,0,0]) => ClockSec[0]
# clock12_to_clock_sec(Clock12[:AM,12,0,1]) => ClockSec[1]
# clock12_to_clock_sec(Clock12[:AM,12,1,0]) => ClockSec[60]
# clock12_to_clock_sec(Clock12[:AM,1,0,0]) => ClockSec[3600]
# clock12_to_clock_sec(Clock12[:AM,11,59,59]) => ClockSec[43199]
# clock12_to_clock_sec(Clock12[:PM,12,0,0]) => ClockSec[43200]
# clock12_to_clock_sec(Clock12[:PM,12,0,1]) => ClockSec[43201]
# clock12_to_clock_sec(Clock12[:PM,12,1,0]) => ClockSec[43260]
# clock12_to_clock_sec(Clock12[:PM,1,0,0]) => ClockSec[46800]
# clock12_to_clock_sec(Clock12[:PM,11,59,59]) => ClockSec[86399]
def clock12_to_clock_sec(clock)
   check_pre((clock.clock12?))
   seconds = (clock.min*MIN_IN_SEC) + clock.sec + ((clock.hour==12) ? 0 : clock.hour*HOUR_IN_SEC)
   ClockSec[ (clock.halve==:AM) ? seconds : seconds+DAY_IN_SEC/2]
end

# clock_sec_to_clock24 ::= (clock) ::
# Clock_sec => Clock24

# clock_sec_to_clock24(ClockSec[0]) => Clock24[0,0,0]
# clock_sec_to_clock24(ClockSec[59]) => Clock24[0,0,59]
# clock_sec_to_clock24(ClockSec[60]) => Clock24[0,1,0]
# clock_sec_to_clock24(ClockSec[3599]) => Clock24[0,59,59]
# clock_sec_to_clock24(ClockSec[3600]) => Clock24[1,00,00]
# clock_sec_to_clock24(ClockSec[86399]) => Clock24[23,59,59]
def clock_sec_to_clock24(clock)
   check_pre((clock.clock_sec?))
   s = clock.seconds.divmod(MIN_IN_SEC)
   m = s[0].divmod(HOUR_IN_MIN)
   h = m[0].divmod(HOURS_OF_DAY)
   Clock24[h[1],m[1],s[1]]
end

# clock_sec_to_clock12 ::= (clock) ::
# Clock_sec => Clock12

# clock_sec_to_clock12(ClockSec[0]) => Clock12[:AM,12,0,0]
# clock_sec_to_clock12(ClockSec[1]) => Clock12[:AM,12,0,1]
# clock_sec_to_clock12(ClockSec[59]) => Clock12[:AM,12,0,59]
# clock_sec_to_clock12(ClockSec[60 => Clock12[:AM,12,1,0]
# clock_sec_to_clock12(ClockSec[3599]) => Clock12[:AM,12,59,59]
# clock_sec_to_clock12(ClockSec[3600]) => Clock12[:AM,1,0,0]
# clock_sec_to_clock12(ClockSec[43199]) => Clock12[:AM,11,59,59]
# clock_sec_to_clock12(ClockSec[43200]) => Clock12[:PM,12,0,0]
# clock_sec_to_clock12(ClockSec[43201]) => Clock12[:PM,12,0,1]
# clock_sec_to_clock12(ClockSec[43260]) => Clock12[:PM,12,1,0]
# clock_sec_to_clock12(ClockSec[86399]) => Clock12[:PM,11,59,59]
def clock_sec_to_clock12(clock)
   check_pre((clock.clock_sec?))
   s = clock.seconds.divmod(MIN_IN_SEC)
   m = s[0].divmod(HOUR_IN_MIN)
   h = m[0].divmod(HOURS_OF_DAY)
   halve = (h[1]>=HOURS_OF_HALF_DAY) ? :PM : :AM
   hours = (h[1]>=HOURS_OF_HALF_DAY) ? h[1]-HOURS_OF_HALF_DAY : h[1]
   Clock12[halve,(hours==0) ? 12 : hours,m[1],s[1]]
end

# clock24_to_clock12 ::= (clock) ::
# Clock24 => Clock12

# clock24_to_clock12(Clock24[0,0,0]) => Clock12[:AM,12,0,0]
# clock24_to_clock12(Clock24[11,59,59]) => Clock12[:AM,11,59,59]
# clock24_to_clock12(Clock24[12,0,0]) => Clock12[:PM,12,0,0]
# clock24_to_clock12(Clock24[23,59,59]) => Clock12[:PM,11,59,59]
def clock24_to_clock12(clock)
   check_pre((clock.clock24?))
   clock_sec_to_clock12(clock24_to_clock_sec(clock))
end

# clock12_to_clock24 ::= (clock) ::
# Clock12 => Clock24

# clock12_to_clock24(Clock12[:AM,12,0,0]) => Clock24[0,0,0]
# clock12_to_clock24(Clock12[:AM,11,59,59]) => Clock24[11,59,59]
# clock12_to_clock24(Clock12[:PM,12,0,0]) => Clock24[12,0,0]
# clock12_to_clock24(Clock12[:PM,11,59,59]) => Clock24[23,59,59]
def clock12_to_clock24(clock)
   check_pre((clock.clock12?))
   clock_sec_to_clock24(clock12_to_clock_sec(clock))
end

################################### Schritt 4

# to_clock_sec ::= (clock) ::
# Clock => ClockSec

# to_clock_sec(ClockSec[0]) => ClockSec[0]
# to_clock_sec(Clock12[:AM,12,0,0]) => ClockSec[0]
# to_clock_sec(Clock24[0,0,0]) => ClockSec[0]
def to_clock_sec(clock)
   if clock.clock24?
      clock24_to_clock_sec(clock)
   elsif clock.clock12?
      clock12_to_clock_sec(clock)
   elsif clock.clock_sec?
      clock
   else
     check_pre(false)
   end
end

# to_clock24 ::= (clock) ::
# Clock => Clock24

# to_clock24(ClockSec[0]) => Clock24[0,0,0]
# to_clock24(Clock12[:AM,12,0,0]) => Clock24[0,0,0]
# to_clock24(Clock24[0,0,0]) => Clock24[0,0,0]
def to_clock24(clock)
   if clock.clock24?
      clock
   elsif clock.clock12?
      clock12_to_clock24(clock)
   elsif clock.clock_sec?
      clock_sec_to_clock24(clock)
   else
     check_pre(false)
   end
end

# to_clock12 ::= (clock) ::
# Clock => Clock12

# to_clock12(ClockSec[0]) => Clock12[:AM,12,0,0]
# to_clock12(Clock12[:AM,12,0,0]) => Clock12[:AM,12,0,0]
# to_clock12(Clock24[0,0,0]) => Clock12[:AM,12,0,0]
def to_clock12(clock)
   if clock.clock24?
      clock24_to_clock12(clock)
   elsif clock.clock12?
      clock
   elsif clock.clock_sec?
      clock_sec_to_clock12(clock)
   else
     check_pre(false)
   end
end

# to_clock ::= (proto,value) :: Clock x Clock -> Clock ::
# (Clock24 x Clock => Clock24 |
# Clock12 x Clock => Clock12 |
# ClockSec x Clock => ClockSec)

# to_clock(ClockSec[0],ClockSec[0]) => ClockSec[0]
# to_clock(ClockSec[0],Clock24[0,0,0]) => ClockSec[0]
# to_clock(ClockSec[0],Clock12[:AM,12,0,0]) => ClockSec[0]
# 
# to_clock(Clock24[0,0,0],ClockSec[0]) => Clock24[0,0,0]
# to_clock(Clock24[0,0,0],Clock24[0,0,0]) => Clock24[0,0,0]
# to_clock(Clock24[0,0,0],Clock12[:AM,12,0,0]) => Clock24[0,0,0]
# 
# to_clock(Clock12[:AM,12,0,0],ClockSec[0]) => Clock12[:AM,12,0,0]
# to_clock(Clock12[:AM,12,0,0],Clock24[0,0,0]) => Clock12[:AM,12,0,0]
# to_clock(Clock12[:AM,12,0,0],Clock12[:AM,12,0,0]) => Clock12[:AM,12,0,0]
def to_clock(target,value)
   if target.clock24?
      to_clock24(value)
   elsif target.clock12?
      to_clock12(value)
   elsif target.clock_sec?
      to_clock_sec(value)
   else
     check_pre(false)
   end
end

################################### Schritt 5

# clock_add :: = (clock1,clock2) ::
# (Clock24 X Clock => Clock24 |
# Clock12 X Clock => Clock12 |
# ClockSec X Clock => ClockSec)

# clock_add(Clock24[13,1,59],Clock24[1,1,1]) => Clock24[14,3,0]
# clock_add(Clock24[13,1,59],Clock12[:AM,1,1,1]) => Clock24[14,3,0] 
# clock_add(Clock24[13,1,59],ClockSec[46861]) => Clock24[14,3,0]
# 
# clock_add(Clock12[:AM,1,1,59],Clock12[:PM,1,1,1]) => Clock12[:PM,2,3,0]
# clock_add(Clock12[:AM,1,1,59],Clock24[13,1,1]) => Clock12[:PM,2,3,0]
# clock_add(Clock12[:AM,1,1,59],ClockSec[46861]) => Clock12[:PM,2,3,0]
#
# clock_add(ClockSec[46919],ClockSec[3581]) => ClockSec[50580]
# clock_add(ClockSec[46919],Clock12[:AM,1,1,1]) => ClockSec[50580]
# clock_add(ClockSec[46919],Clock24[1,1,1]) => ClockSec[50580]

def clock_add(clock1,clock2)
   to_clock(clock1,clock_sec_add( to_clock_sec(clock1), to_clock_sec(clock2)))
end

# clock_sub :: = (clock1,clock2) ::
# (Clock24 X Clock => Clock24 |
# Clock12 X Clock => Clock12 |
# ClockSec X Clock => ClockSec)

# clock_sub(Clock24[14,3,0],Clock24[1,1,1]) => Clock24[13,1,59]
# clock_sub(Clock24[14,3,0],Clock12[:AM,1,1,1]) => Clock24[13,1,59] 
# clock_sub(Clock24[14,3,0],ClockSec[46861]) => Clock24[13,1,59]
# 
# clock_sub(Clock12[:PM,2,3,0],Clock12[:PM,1,1,1]) => Clock12[:AM,1,1,59]
# clock_sub(Clock12[:PM,2,3,0],Clock24[13,1,1]) => Clock12[:AM,1,1,59]
# clock_sub(Clock12[:PM,2,3,0],ClockSec[46861]) => Clock12[:AM,1,1,59]
#
# clock_sub(ClockSec[50580],ClockSec[3581]) => ClockSec[46919]
# clock_sub(ClockSec[50580],Clock12[:AM,1,1,1]) => ClockSec[46919]
# clock_sub(ClockSec[50580],Clock24[1,1,1]) => ClockSec[46919]

def clock_sub(clock1,clock2)
  to_clock(clock1,clock_sec_sub( to_clock_sec(clock1), to_clock_sec(clock2)))
end

# clock_succ :: = (clock) ::
# (Clock24 => Clock24 |
# Clock12 => Clock12 |
# ClockSec => ClockSec)
# 
# clock_succ(Clock24[13,1,59]) => Clock24[13,2,0]
# clock_succ(Clock12[:PM,1,1,59]) => Clock12[:PM,1,2,0]
# clock_succ(ClockSec[46919]) => ClockSec[46920]

def clock_succ(clock)
   to_clock(clock,clock_sec_succ(to_clock_sec(clock)))
end

# clock_pred :: = (clock) ::
# (Clock24 => Clock24 |
# Clock12 => Clock12 |
# ClockSec => ClockSec)

# clock_pred(Clock24[13,2,0]) => Clock24[13,1,59]
# clock_pred(Clock12[:PM,1,2,0]) => Clock12[:PM,1,1,59]
# clock_pred(ClockSec[46920]) => ClockSec[46919]

def clock_pred(clock)
   to_clock(clock,clock_sec_pred(to_clock_sec(clock)))
end

# clock_hour24 ::= (clock) ::
# (Clock24 => Clock24.hour |
# Clock12 => Clock24.hour |
# ClockSec => Clock24.hour)

# clock_hour24(Clock24[13,0,0]) => 13
# clock_hour24(Clock12[:PM,1,0,0]) => 13
# clock_hour24(Clock12[:AM,1,0,0]) => 1
# clock_hour24(ClockSec[3600]) => 1
# clock_hour24(ClockSec[3599]) => 1

def clock_hour24(clock)
  to_clock24(clock).hour
end

# clock_hour12 ::= (clock) ::
# (Clock24 => Clock12.hour |
# Clock12 => Clock12.hour |
# ClockSec => Clock12.hour)

# clock_hour12(Clock24[1,0,0]) => 1
# clock_hour12(Clock12[:PM,1,0,0]) => 1
# clock_hour12(Clock12[:AM,1,0,0]) => 1
# clock_hour12(ClockSec[3600]) => 1
# clock_hour12(ClockSec[3599]) => 12

def clock_hour12(clock)
  to_clock12(clock).hour
end

# clock_halve ::= (clock) ::
# (Clock24 => Clock12.halve |
# Clock12 => Clock12.halve |
# ClockSec => Clock12.halve)

# clock_halve(Clock24[12,0,0]) => :PM
# clock_halve(Clock24[11,59,59]) => :AM
# clock_halve(Clock12[:PM,12,0,0]) => :PM
# clock_halve(Clock12[:AM,11,59,59]) => :AM
# clock_halve(ClockSec[43200]) => :PM
# clock_halve(ClockSec[1]) => :AM

def clock_halve(clock)
  to_clock12(clock).halve
end

# clock_min ::= (clock) ::
# (Clock24 => Clock24.min |
# Clock12 => Clock24.min |
# ClockSec => Clock24.min)

# clock_min(Clock24[0,1,59]) => 1
# clock_min(Clock12[:AM,12,1,59]) => 1
# clock_min(ClockSec[60]) => 1
# clock_min(ClockSec[59]) => 0

def clock_min(clock)
  to_clock24(clock).min
end

# clock_sec ::= (clock) ::
# (Clock24 => Clock24.sec |
# Clock12 => Clock24.sec |
# ClockSec => Clock24.sec)

# clock_sec(Clock24[0,0,59]) => 59
# clock_sec(Clock12[:AM,12,0,59]) => 59
# clock_sec(ClockSec[1]) => 1
# clock_sec(ClockSec[60]) => 0

def clock_sec(clock)
  to_clock24(clock).sec
end 